
module Query where

import Data.Set as Set
import RPTypes
import SParser hiding (mtrace)
import Control.Monad.Error
import Data.Either

{- 

Notes on query reprocessing:

Phases:

1. Move negation to the bottom
2. Move existentially and universally quantified variables to the top, merge term; rename variables in the process
2a. Unify the quantifiers
2b. Fix the empty pairs of quantifiers in the reperesntation (should this be fone before 2a?)
3. Move universally quantified variables to just above first UQV / negation.
4. Check that negation sits just below first UQV.

-}

import Debug.Trace
mtrace x = (trace ("MTRACE: " ++ (show x)) x)

--instance Error ParseError where

normalizeQueryPM :: Term -> ParseMonad (CBody,CBody,CBody)
normalizeQueryPM qt = 
    do cb <- clauseBody qt
       return (phase3 $ phase2b $ phase2a $ fst $ phase2 $ phase1 $ cb)

{-
-- no errorhandling version
normalizeQuery :: Term -> IO (CBody,CBody,CBody)
normalizeQuery qt =
    return (fromRight ((normalizeQueryPM qt) `catchError` printError))
    where printError e = return (CNIL,CNIL,CNIL)
-}

normalizeQuery :: Term -> IO (CBody,CBody,CBody)
normalizeQuery qt =
    let qr = (normalizeQueryPM qt)
    in (return (fromRight qr)) `catchError` printError
    where printError e = 
                  do throwError e

nqtest q = let p1 = phase1 q
               (p2,t2) = phase2 p1
           in print p1


phase1 :: CBody -> CBody
phase1 (CNOT (CNOT b _) _) = phase1 b
phase1 (CNOT (CCONJ x y _) _) = (CDISJ (phase1 (CNOT x Notset)) (phase1 (CNOT y Notset)) Notset)
phase1 (CNOT (CDISJ x y _) _) = (CCONJ (phase1 (CNOT x Notset)) (phase1 (CNOT y Notset)) Notset)
phase1 (CNOT (CQUANT q b _) _) = (CQUANT (revq q) (phase1 (CNOT b Notset)) Notset)
phase1 (CDISJ x y _) = (CDISJ (phase1 x) (phase1 y) Notset)
phase1 (CCONJ x y _) = (CCONJ (phase1 x) (phase1 y) Notset)
phase1 (CQUANT v b _) = (CQUANT v (phase1 b)  Notset)
phase1 x = x

revq q = (Set.empty:q)

-- this is similar to a bubblesort, pulling the CQUANTs to the top,
--  and should have n log n complexity.

-- postcondition, the result of this function will have all CQUANTs up the top.

-- set frees in here ...

phase2 :: CBody -> (CBody,Set Term) -- returns a normalized clause body and a collection of free variables

phase2 (CNOT x _) = 
    let (b,v) = phase2 x -- no quants inside because of phase1; XXX be careful for modification!
    in ((CNOT b (LV v)),v)
phase2 (CCONJ x y _) = phase2binop x y CCONJ
phase2 (CDISJ x y _) = phase2binop x y CDISJ
phase2 (CTERM x _) = ((CTERM x (LV $ freeVars x)),freeVars x)
phase2 CNIL = (CNIL, Set.empty)
phase2 (CQUANT vq b _) = 
    let (bp, vs) = phase2 b
        vv = Set.difference vs (Set.unions vq)
    in ((CQUANT vq bp (LV vv)), vv) -- delete the variables in the qunatifier from the frees

phase2binop x y op =
    let (xb,xv) = (phase2 x)
        (yb,yv) = (phase2 y)
        names = Set.union xv yv
    in (mergeQuant ((phase2a xb),xv) ((phase2a yb),yv) op (LV names),names)

-- for phase 2 
mergeQuant :: (CBody,Set Term) -> (CBody,Set Term) -> (CBody -> CBody -> Frees -> CBody) -> Frees -> (CBody)
{-
mergeQuant (CQUANT  b1) (CQUANT  b2) op = --- XXX generalize to mult vars
    let e1 = Set.fromList el1
        e2 = Set.fromList el2
        u1 = Set.fromList ul1
        u2 = Set.fromList ul2
        commExist = Set.intersection e1 e2
        commUniv = Set.intersection u1 u2
        (bb2,eb2) = renameVariables renamer commExist b2
        (bbb2,ub2) = renameVariables renamer commUniv b2
        ef = Set.union (Set.union e1 (Set.difference e2 e1)) eb2
        uf = Set.union (Set.union u1 (Set.difference u2 u1)) ub2
    in (CQUANT [(Set.toList ef),(Set.toList uf)] (op b1 bbb2))
-}
mergeQuant ((CQUANT [] b1 _),fv1) rest@((CQUANT q2 b2 _),fv2) op names = mergeQuant (b1,fv1) rest op names
mergeQuant rest@((CQUANT q1 b1 _),fv1) ((CQUANT [] b2 _),fv2) op names = mergeQuant rest (b2,fv2) op names
mergeQuant ((CQUANT qv b1 _),_) (x,fvx) op names = (CQUANT newqv (op newb x names) names) 
                                           where (newqv,newb) = renameTail fvx qv b1
mergeQuant (x,fvx) ((CQUANT qv b1 _),_) op names = (CQUANT newqv (op x newb names) names)
                                           where (newqv,newb) = renameTail fvx qv b1
mergeQuant (x,_) (y,_) op n = (op x y n) -- already guaranteed that free variables are separated in phasebinhop

-- rename the variables in the tail
renameTail :: Set Term -> [Set Term] -> CBody -> ([Set Term],CBody)
renameTail _ [] b = ([],b)
renameTail fvx (q:qs) b = ((fq:fqs),fb)
    where (fqs,fb0) = renameTail fvx qs b
          renames = (Set.intersection q fvx)
          (fb,newq) = renameVariables renamer renames fb0
          fq = (Set.union newq (Set.difference q fvx)) --- XXX real bug here

{-
Mergequant; several stages;

- final stage is a call to the base case, which renames closed common variables
- recursive stage, identify common varibles in qunatifier sets, and rename common
  variables 

-}

renameVariables :: (Term -> Term) -> (Set Term) -> CBody -> (CBody, Set Term)
renameVariables map vars (CDISJ x y _) = 
    let (xb,xv) = renameVariables map vars x
        (yb,yv) = renameVariables map vars y
    in ((CDISJ xb yb (LV$Set.union xv yv)),(Set.union xv yv))
renameVariables map vars (CCONJ x y _) = 
    let (xb,xv) = renameVariables map vars x
        (yb,yv) = renameVariables map vars y
    in ((CCONJ xb yb (LV$Set.union xv yv)),(Set.union xv yv))
renameVariables map vars (CNIL) = (CNIL,Set.empty)
renameVariables map vars (CQUANT qv b _) = 
    let (bb,bv) = renameVariables map vars b
    in ((CQUANT qv bb (LV bv)),bv)
renameVariables map vars (CTERM t _) = 
    let (tp,v) = renameVT map vars t
    in ((CTERM tp (LV v)),v)
renameVariables map vars (CNOT b _) =
    let (bb,bv) = renameVariables map vars b
    in ((CNOT bb (LV bv)),bv)

renameVT :: (Term -> Term) -> (Set Term) -> Term -> (Term,Set Term)
renameVT map vars (T at ar s p) = 
    let (ss,sv) = foldl ( \(ls,lv) t -> let (ns,nv) = renameVT map vars t in (ns:ls,Set.union lv nv)) ([],Set.empty) s
    in ((T at ar ss p),sv)
renameVT map vars (V x p) =
    if Set.member (V x p) vars
    then (map (V x p),Set.fromList [map (V x p)])
    else ((V x p),Set.empty)
renameVT map vars x = (x,Set.empty)

freeVars (T _ _ s _ ) = foldl (\v t -> Set.union v (freeVars t)) Set.empty s
freeVars (V x c) = Set.fromList [(V x c)]

renamer (V x p) = (V (x ++ "p") p)

--- phase2a --- postcondition; at most one CQUANT, which must be up the top

phase2a :: CBody -> CBody

phase2a (CQUANT q1 (CQUANT q2 b _) fv) = phase2a (CQUANT (mergeVars q1 q2) b fv)
phase2a x = x


-- four Cases: l1 even or not, l2 starts with [] or not.

mergeVars :: [Set Term] -> [Set Term] -> [Set Term]
mergeVars l1 l2 
       | l1even       && l2se = mergestartfinal l1 l2
       | (not l1even) && l2se = (l1 ++ (tail l2))
       | l1even && (not l2se) = (l1 ++ l2)
       | (not l1even) && (not l2se) = mergestartfinal l1 l2
       where l1even = ((length l1) `mod` 2) == 0
             l2se = Set.null (head l2)

mergestartfinal :: [Set Term] -> [Set Term] -> [Set Term]
mergestartfinal l1 l2 = sl1 ++ (el1 ++ hl2) ++ tl2
                        where (sl1p,el1) = splitAt 1 (reverse l1)
                              (hl2,tl2) = splitAt 1 l2
                              sl1 = reverse sl1p

phase2b (CQUANT v b fv) = (CQUANT (deleteEmptyPairs v) b fv)
phase2b x = x

deleteEmptyPairs (a:(b:r)) = 
    if (Set.null a) && (Set.null b) 
       then deleteEmptyPairs r
       else a:(deleteEmptyPairs (b:r))
deleteEmptyPairs [] = []
deleteEmptyPairs (t:r) = t:(deleteEmptyPairs r)

phase3 (CQUANT [e,f] b fv) = 
    let (full,ded,ind) = (p3 f b)
    in ((CQUANT [e] full fv),ded,ind)
-- phase3 _ = throw an error here

p3 f b@(CCONJ b1 b2 fv)
   | Set.null(Set.intersection (freevars b1) f) = 
       let (full,ded,ind) = (p3 f b2)
       in ((CCONJ b1 full fv),(CCONJ b1 ded fv),ind)
   | otherwise = ((CQUANT [efv,f] b fv),CNIL,b)
p3 f b@(CDISJ b1 b2 fv)
   | Set.null(Set.intersection (freevars b1) f) = 
       let (full,ded,ind) = (p3 f b2)
       in ((CDISJ b1 full fv),(CDISJ b1 ded fv),ind)
   | otherwise = ((CQUANT [efv,f] b fv),CNIL,b)
p3 f b@(CNOT bb fv)= ((CQUANT [efv,f] bb fv),CNIL,b)
--- won't even bother with CQUANT
p3 f b@(CTERM t fv) =((CQUANT [efv,f] b fv),CNIL,b)


efv = Set.empty